Efficient Satisfiability Modulo Theories via Delayed Theory Combination
Identifieur interne : 006263 ( Main/Exploration ); précédent : 006262; suivant : 006264Efficient Satisfiability Modulo Theories via Delayed Theory Combination
Auteurs : Marco Bozzano [Italie] ; Roberto Bruttomesso [Italie] ; Alessandro Cimatti [Italie] ; Tommi Junttila [Finlande] ; Silvio Ranise [France] ; Peter Van Rossum [Pays-Bas] ; Roberto Sebastiani [Italie]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
Descripteurs français
- Pascal (Inist)
- Analyse non convexe, Architecture logiciel, Disjonction, Enumération, Logique booléenne, Logique propositionnelle, Modélisation, Multitâche, Niveau transfert registre, Prise décision, Problème satisfiabilité, Processeur pipeline, Quantificateur, Retard, Satisfiabilité, Simultanéité informatique, Théorie preuve, Vérification programme.
English descriptors
- KwdEn :
Abstract
Abstract: The problem of deciding the satisfiability of a quantifier-free formula with respect to a background theory, also known as Satisfiability Modulo Theories (SMT), is gaining increasing relevance in verification: representation capabilities beyond propositional logic allow for a natural modeling of real-world problems (e.g., pipeline and RTL circuits verification, proof obligations in software systems). In this paper, we focus on the case where the background theory is the combination T 1∪T 2 of two simpler theories. Many SMT procedures combine a boolean model enumeration with a decision procedure for T 1∪T 2, where conjunctions of literals can be decided by an integration schema such as Nelson-Oppen, via a structured exchange of interface formulae (e.g., equalities in the case of convex theories, disjunctions of equalities otherwise). We propose a new approach for SMT(T 1∪T 2), called Delayed Theory Combination, which does not require a decision procedure for T 1∪T 2, but only individual decision procedures for T 1 and T 2, which are directly integrated into the boolean model enumerator. This approach is much simpler and natural, allows each of the solvers to be implemented and optimized without taking into account the others, and it nicely encompasses the case of non-convex theories. We show the effectiveness of the approach by a thorough experimental comparison.
Url:
DOI: 10.1007/11513988_34
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 000F37
- to stream Istex, to step Curation: 000F23
- to stream Istex, to step Checkpoint: 001577
- to stream Main, to step Merge: 006488
- to stream PascalFrancis, to step Corpus: 000543
- to stream PascalFrancis, to step Curation: 000495
- to stream PascalFrancis, to step Checkpoint: 000500
- to stream Main, to step Merge: 006637
- to stream Main, to step Curation: 006263
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Efficient Satisfiability Modulo Theories via Delayed Theory Combination</title><author><name sortKey="Bozzano, Marco" sort="Bozzano, Marco" uniqKey="Bozzano M" first="Marco" last="Bozzano">Marco Bozzano</name></author><author><name sortKey="Bruttomesso, Roberto" sort="Bruttomesso, Roberto" uniqKey="Bruttomesso R" first="Roberto" last="Bruttomesso">Roberto Bruttomesso</name></author><author><name sortKey="Cimatti, Alessandro" sort="Cimatti, Alessandro" uniqKey="Cimatti A" first="Alessandro" last="Cimatti">Alessandro Cimatti</name></author><author><name sortKey="Junttila, Tommi" sort="Junttila, Tommi" uniqKey="Junttila T" first="Tommi" last="Junttila">Tommi Junttila</name></author><author><name sortKey="Ranise, Silvio" sort="Ranise, Silvio" uniqKey="Ranise S" first="Silvio" last="Ranise">Silvio Ranise</name></author><author><name sortKey="Van Rossum, Peter" sort="Van Rossum, Peter" uniqKey="Van Rossum P" first="Peter" last="Van Rossum">Peter Van Rossum</name></author><author><name sortKey="Sebastiani, Roberto" sort="Sebastiani, Roberto" uniqKey="Sebastiani R" first="Roberto" last="Sebastiani">Roberto Sebastiani</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:413EE9A4C2AFD16BD40056910219928802E51CDA</idno><date when="2005" year="2005">2005</date><idno type="doi">10.1007/11513988_34</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-TR9Z5WSX-Q/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">000F37</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">000F37</idno><idno type="wicri:Area/Istex/Curation">000F23</idno><idno type="wicri:Area/Istex/Checkpoint">001577</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">001577</idno><idno type="wicri:doubleKey">0302-9743:2005:Bozzano M:efficient:satisfiability:modulo</idno><idno type="wicri:Area/Main/Merge">006488</idno><idno type="wicri:source">INIST</idno><idno type="RBID">Pascal:05-0349607</idno><idno type="wicri:Area/PascalFrancis/Corpus">000543</idno><idno type="wicri:Area/PascalFrancis/Curation">000495</idno><idno type="wicri:Area/PascalFrancis/Checkpoint">000500</idno><idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000500</idno><idno type="wicri:doubleKey">0302-9743:2005:Bozzano M:efficient:satisfiability:modulo</idno><idno type="wicri:Area/Main/Merge">006637</idno><idno type="wicri:Area/Main/Curation">006263</idno><idno type="wicri:Area/Main/Exploration">006263</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Efficient Satisfiability Modulo Theories via Delayed Theory Combination</title><author><name sortKey="Bozzano, Marco" sort="Bozzano, Marco" uniqKey="Bozzano M" first="Marco" last="Bozzano">Marco Bozzano</name><affiliation wicri:level="1"><country xml:lang="fr">Italie</country><wicri:regionArea>ITC-IRST, Povo, Trento</wicri:regionArea><wicri:noRegion>Trento</wicri:noRegion></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Italie</country></affiliation></author><author><name sortKey="Bruttomesso, Roberto" sort="Bruttomesso, Roberto" uniqKey="Bruttomesso R" first="Roberto" last="Bruttomesso">Roberto Bruttomesso</name><affiliation wicri:level="1"><country xml:lang="fr">Italie</country><wicri:regionArea>ITC-IRST, Povo, Trento</wicri:regionArea><wicri:noRegion>Trento</wicri:noRegion></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Italie</country></affiliation></author><author><name sortKey="Cimatti, Alessandro" sort="Cimatti, Alessandro" uniqKey="Cimatti A" first="Alessandro" last="Cimatti">Alessandro Cimatti</name><affiliation wicri:level="1"><country xml:lang="fr">Italie</country><wicri:regionArea>ITC-IRST, Povo, Trento</wicri:regionArea><wicri:noRegion>Trento</wicri:noRegion></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Italie</country></affiliation></author><author><name sortKey="Junttila, Tommi" sort="Junttila, Tommi" uniqKey="Junttila T" first="Tommi" last="Junttila">Tommi Junttila</name><affiliation wicri:level="1"><country xml:lang="fr">Finlande</country><wicri:regionArea>Helsinki University of Technology</wicri:regionArea></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Finlande</country></affiliation></author><author><name sortKey="Ranise, Silvio" sort="Ranise, Silvio" uniqKey="Ranise S" first="Silvio" last="Ranise">Silvio Ranise</name><affiliation wicri:level="1"><country xml:lang="fr">France</country><wicri:regionArea>LORIA and INRIA-Lorraine, Villers les Nancy</wicri:regionArea><wicri:noRegion>Villers les Nancy</wicri:noRegion><wicri:noRegion>Villers les Nancy</wicri:noRegion></affiliation><affiliation wicri:level="1"><country wicri:rule="url">France</country></affiliation></author><author><name sortKey="Van Rossum, Peter" sort="Van Rossum, Peter" uniqKey="Van Rossum P" first="Peter" last="Van Rossum">Peter Van Rossum</name><affiliation wicri:level="3"><country xml:lang="fr">Pays-Bas</country><wicri:regionArea>Radboud University, Nijmegen</wicri:regionArea><placeName><settlement type="city">Nimègue</settlement><region type="province" nuts="2">Gueldre</region></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Pays-Bas</country></affiliation></author><author><name sortKey="Sebastiani, Roberto" sort="Sebastiani, Roberto" uniqKey="Sebastiani R" first="Roberto" last="Sebastiani">Roberto Sebastiani</name><affiliation wicri:level="1"><country xml:lang="fr">Italie</country><wicri:regionArea>DIT, Università di Trento</wicri:regionArea><wicri:noRegion>Università di Trento</wicri:noRegion></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Italie</country></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><idno type="ISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Boolean logic</term><term>Concurrency</term><term>Decision making</term><term>Delay</term><term>Disjunction</term><term>Enumeration</term><term>Modeling</term><term>Multithread</term><term>Non convex analysis</term><term>Pipeline processor</term><term>Program verification</term><term>Proof theory</term><term>Propositional logic</term><term>Quantifier</term><term>Register transfer level</term><term>Satisfiability</term><term>Satisfiability problem</term><term>Software architecture</term></keywords><keywords scheme="Pascal" xml:lang="fr"><term>Analyse non convexe</term><term>Architecture logiciel</term><term>Disjonction</term><term>Enumération</term><term>Logique booléenne</term><term>Logique propositionnelle</term><term>Modélisation</term><term>Multitâche</term><term>Niveau transfert registre</term><term>Prise décision</term><term>Problème satisfiabilité</term><term>Processeur pipeline</term><term>Quantificateur</term><term>Retard</term><term>Satisfiabilité</term><term>Simultanéité informatique</term><term>Théorie preuve</term><term>Vérification programme</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: The problem of deciding the satisfiability of a quantifier-free formula with respect to a background theory, also known as Satisfiability Modulo Theories (SMT), is gaining increasing relevance in verification: representation capabilities beyond propositional logic allow for a natural modeling of real-world problems (e.g., pipeline and RTL circuits verification, proof obligations in software systems). In this paper, we focus on the case where the background theory is the combination T 1∪T 2 of two simpler theories. Many SMT procedures combine a boolean model enumeration with a decision procedure for T 1∪T 2, where conjunctions of literals can be decided by an integration schema such as Nelson-Oppen, via a structured exchange of interface formulae (e.g., equalities in the case of convex theories, disjunctions of equalities otherwise). We propose a new approach for SMT(T 1∪T 2), called Delayed Theory Combination, which does not require a decision procedure for T 1∪T 2, but only individual decision procedures for T 1 and T 2, which are directly integrated into the boolean model enumerator. This approach is much simpler and natural, allows each of the solvers to be implemented and optimized without taking into account the others, and it nicely encompasses the case of non-convex theories. We show the effectiveness of the approach by a thorough experimental comparison.</div></front></TEI><affiliations><list><country><li>Finlande</li><li>France</li><li>Italie</li><li>Pays-Bas</li></country><region><li>Gueldre</li></region><settlement><li>Nimègue</li></settlement></list><tree><country name="Italie"><noRegion><name sortKey="Bozzano, Marco" sort="Bozzano, Marco" uniqKey="Bozzano M" first="Marco" last="Bozzano">Marco Bozzano</name></noRegion><name sortKey="Bozzano, Marco" sort="Bozzano, Marco" uniqKey="Bozzano M" first="Marco" last="Bozzano">Marco Bozzano</name><name sortKey="Bruttomesso, Roberto" sort="Bruttomesso, Roberto" uniqKey="Bruttomesso R" first="Roberto" last="Bruttomesso">Roberto Bruttomesso</name><name sortKey="Bruttomesso, Roberto" sort="Bruttomesso, Roberto" uniqKey="Bruttomesso R" first="Roberto" last="Bruttomesso">Roberto Bruttomesso</name><name sortKey="Cimatti, Alessandro" sort="Cimatti, Alessandro" uniqKey="Cimatti A" first="Alessandro" last="Cimatti">Alessandro Cimatti</name><name sortKey="Cimatti, Alessandro" sort="Cimatti, Alessandro" uniqKey="Cimatti A" first="Alessandro" last="Cimatti">Alessandro Cimatti</name><name sortKey="Sebastiani, Roberto" sort="Sebastiani, Roberto" uniqKey="Sebastiani R" first="Roberto" last="Sebastiani">Roberto Sebastiani</name><name sortKey="Sebastiani, Roberto" sort="Sebastiani, Roberto" uniqKey="Sebastiani R" first="Roberto" last="Sebastiani">Roberto Sebastiani</name></country><country name="Finlande"><noRegion><name sortKey="Junttila, Tommi" sort="Junttila, Tommi" uniqKey="Junttila T" first="Tommi" last="Junttila">Tommi Junttila</name></noRegion><name sortKey="Junttila, Tommi" sort="Junttila, Tommi" uniqKey="Junttila T" first="Tommi" last="Junttila">Tommi Junttila</name></country><country name="France"><noRegion><name sortKey="Ranise, Silvio" sort="Ranise, Silvio" uniqKey="Ranise S" first="Silvio" last="Ranise">Silvio Ranise</name></noRegion><name sortKey="Ranise, Silvio" sort="Ranise, Silvio" uniqKey="Ranise S" first="Silvio" last="Ranise">Silvio Ranise</name></country><country name="Pays-Bas"><region name="Gueldre"><name sortKey="Van Rossum, Peter" sort="Van Rossum, Peter" uniqKey="Van Rossum P" first="Peter" last="Van Rossum">Peter Van Rossum</name></region><name sortKey="Van Rossum, Peter" sort="Van Rossum, Peter" uniqKey="Van Rossum P" first="Peter" last="Van Rossum">Peter Van Rossum</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 006263 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 006263 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:413EE9A4C2AFD16BD40056910219928802E51CDA
|texte= Efficient Satisfiability Modulo Theories via Delayed Theory Combination
}}
| This area was generated with Dilib version V0.6.33. |  |